Type Systems
------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [PLDI](../PLDI/README.md#pldi), [Type Theory](../Type%20Theory/README.md#type-theory)_

- - - -


### Web resources

[type safety - What is the difference between a strongly typed language and a statically typed language? - Stack Overflow](https://stackoverflow.com/questions/2690544/what-is-the-difference-between-a-strongly-typed-language-and-a-statically-typed#2696369) ★★★

[What is a strictly typed language? - Stack Overflow](https://stackoverflow.com/questions/805168/what-is-a-strictly-typed-language) ★

[Coeffects: The next big programming challenge - Tomas Petricek](http://tomasp.net/blog/2014/why-coeffects-matter/) ★

[Type Constraints · The Programming Languages Laboratory](https://www.pl.cs.jhu.edu/projects/type-constraints/) ★

[The algebra (and calculus!) of algebraic data types](https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types) ★★★

[What is a type and effect system? - Stack Overflow](https://stackoverflow.com/questions/196465/what-is-a-type-and-effect-system) ★

_(in [PLDI](../PLDI/README.md#pldi))_ [language design - Why F\#, Rust and Others Use Option Type Instead Of Nullable types like C\# 8 Or TypeScript? - Software Engineering Stack Exchange](https://softwareengineering.stackexchange.com/questions/410724/why-f-rust-and-others-use-option-type-instead-of-nullable-types-like-c-8-or-t) ★

_(in [Python](../Python/README.md#python))_ [Specification for the Python type system — typing documentation](https://typing.readthedocs.io/en/latest/spec/) ★


### Papers

Should Your Specification Language Be Typed? (online @ [lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#should-your-specification-language-be-typed)

On Understanding Data Abstraction, Revisited (online @ [cs.utexas.edu](https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#on-understanding-data-abstraction-revisited)

In Search of Types (online @ [kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/srk21/papers/kell14in-author-version.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#in-search-of-types)

Several types of types in programming languages (online @ [arxiv.org](https://arxiv.org/abs/1510.03726)) ★ [💭](commentary/Chris%20Pressey.md#several-types-of-types-in-programming-languages)

Unfolding Abstract Datatypes (online @ [www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#unfolding-abstract-datatypes)

Initial Algebra Semantics is Enough! (online @ [libres.uncg.edu](https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2007_Intitial%20Algebra%20Semantics%20Is%20Enough.pdf)) ★ [💭](commentary/Chris%20Pressey.md#initial-algebra-semantics-is-enough)

Type and Effect Systems (online @ [web.cs.ucla.edu](https://web.cs.ucla.edu/~palsberg/tba/papers/nielson-nielson-csd99.pdf)) ★

A Theory of Type Polymorphism in Programming (online @ [homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/milner-type-polymorphism.pdf)) 🏛️

Abstract Types have Existential Type (online @ [homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf)) 🏛️

_(in [Haskell](../Haskell/README.md#haskell))_ Faking it (online @ [www.cambridge.org](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/faking-it-simulating-dependent-types-in-haskell/A904B84CA962F2D75578445B703F199A)) ★ [💭](commentary/Chris%20Pressey.md#faking-it)


### Books

Counterexamples in Type Systems (online @ [counterexamples.org](https://counterexamples.org/)) ★★